COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	provin[boo,jmc]
C00004 ENDMK
C⊗;
provin[boo,jmc]
if false then begin "what is needed"
s(PROVIN,PROVING FACTS ABOUT LISP PROGRAMS)
ss(formal,About Formalizing.)
ss(sexpth, The theory of S-expressions.)
ss(first, Summary of notion of formal theory.)
ss(lispth, |Lists, natural numbers and LISP program primitives.|)
ss(total,Representing programs known to terminate.)
ss(partial,Representing programs not known to terminate.)
ss(recpred,Recursively Defined Predicates.)
ss(induction, Additional induction principles for proving.)
ss(minim,Partial functions and the Minimization Schema.)
ss(lispax,Theory of LISP: Algebraic Axioms.)
next page
00169 ENDMK
⊗;

1. First order logic (skippable if the student already knows the language
of first order logic)
2. extensions to first order logic. conditional expressions, first order
lambda-expressions
3. the problems of representing lisp programs in first order logic
	non-termination
	terminating programs
	functionals and fixed points
	use of bottom to represent possibly non-terminating programs
	the two kinds of conditional expression